Nuprl Lemma : R-sends-rule 11,40

k:Knd, T:Type, l:IdLnk, ds,dt:fpf(Id; tg.Type),
g:((tg:Id  (decl-state(ds)T(decl-type{i:l}(dttg) List))) List).
((isrcv(k))
 ((destination(lnk(k)) = source(l Id)
  ((eq_lnk(lnk(k); l))  (T = decl-type{i:l}(dt; tag(k))))))
 normal-ds{i:l}
 normal-ds(ds)
 normal-type{i:l}
 normal-type(T)
 normal-ds{i:l}
 normal-ds(dt)
 R-realizes{i:l}
 R-realizes(Rsends(dskTldtg); es.sends-p(esdskTldtg)) 
latex


Definitionsxt(x), prop{i:l}, t  T, A c B, R-Feasible{i:l}(R), R-realizes{i:l}(Res.P(es)), P  Q, P  Q, x:AB(x), x(s), R-consistent(Res), normal-type{i:l}(T), normal-ds{i:l}(ds), decl-type{i:l}(dsx)
LemmasKnd wf, IdLnk wf, fpf wf, decl-state wf, tagof wf, decl-type wf, lsrc wf, ldst wf, Id wf, isrcv wf, normal-type wf, normal-ds wf, event system wf, Rsends wf, R-consistent wf, lnk wf, eq lnk wf, assert wf

origin